Programación Avanzada

1 Contenido de la clase

¿Qué es demostrar formalmente un programa?

La demostración formal de programas es la aplicación de técnicas, métodos y resultados formales a un programa para demostrar que funciona correctamente. ¿En qué sentido un programa es correcto? Si se tiene un conjunto de datos de entrada P para un programa C, entonces si al ejecutarlo se obtiene un conjunto de datos Q que es el esperado, el programa es correcto: hace lo que tiene que hacer. En este sentido de programa correcto no se toma en cuenta: el tiempo de ejecución, los recursos utilizados ni el código eficiente.

Las ternas de Hoare

Uno de los métodos formales de demostración son las Ternas de Hoare. Su creador, Charles Antony Richard Hoare, nació el 11 de enero de 1934 en Colombo, Sri Lanka; inventó QuickSort en 1960, recibió el Premio Turing en 1980 y actualmente trabaja en Microsoft.

El método consiste en hacer un proceso de inferencia lógica para cada tipo de instrucción ejecutable: por eso, para cada tipo de instrucción existe una regla de inferencia. Cada regla asume un conjunto previo de condiciones, llamadas precondiciones; tras aplicar la regla se genera otro conjunto, llamado poscondiciones. Por ello el método también se conoce como precondiciones y poscondiciones de Hoare. Las precondiciones y poscondiciones establecen valores de variables y también se les llama aserciones o aseveraciones.

Ejemplos: { x = 3, y ≤ z, z > 4 }; la aseveración vacía { } (no compromete nada); { a = b, i ≠ j }. Las precondiciones se denotan {P} y las poscondiciones {Q}, donde P y Q son conjuntos de relaciones entre variables y constantes.

Código, estados y aserciones

Si C es una parte del código (desde una sentencia hasta un programa completo):

• Cualquier aserción {P} se denomina precondición de C si {P} solo implica el estado inicial.
• Cualquier aserción {Q} se denomina postcondición si solo implica el estado final (la aseveración después de ejecutar C).
• La concatenación de dos códigos C1 y C2 se representa como C1 ; C2.

Un estado es el conjunto de valores que toman en un instante las variables de la estructura de datos del código. Un programa es una secuencia de instrucciones que transforma un estado inicial en un estado final. Un estado E satisface una aseveración P cuando los valores de las variables en E se cumplen en P: por ejemplo, el estado E = { x = 2 } satisface la aseveración P = { x ≥ 2 }, pero el estado E = { x ≥ 2 } no satisface P = { x = 2 } (por ejemplo, x = 5 no cumple x = 2).

Las precondiciones establecen las condiciones que deben cumplir los datos de entrada; las postcondiciones establecen las condiciones de salida aceptadas como soluciones correctas. Ejemplo: programa que calcula la raíz cuadrada de un número: precondición = que el número no sea negativo; postcondición = la raíz cuadrada del número.

Las ternas {P} C {Q} y la aserción vacía

Una terna de Hoare está formada por {P} C {Q}. Ejemplos: { y ≠ 0 } x := 1/y { x = 1/y } y { } a := b { a = b } (sin precondición: siempre se obtienen estados que satisfacen la postcondición).

La aserción vacía { } se entiende como "verdadera para todos los estados" y satisface cualquier aseveración. Algunas propiedades: si P es una aseveración cualquiera, { } ∧ P = P; { } ∨ P = { }; { k = k } = { }; { C/2 + 1 = C/2 + 1 } = { }; { (a + b) = (a + b) } = { }.

La terna {P} C {Q} es correcta si cada estado inicial que satisfaga {P} produce un estado final que satisface {Q} después de ejecutar C.

Corrección parcial y total

• Corrección parcial: {P} C {Q} es parcialmente correcto si el estado final de C, cuando termina el programa (aunque no se le exige que termine), satisface {Q} siempre que el estado inicial satisfaga {P}.
• Corrección total: además de ser parcialmente correcto, el código siempre termina.

Los programas sin ciclos siempre terminan, por lo que en esos casos la corrección parcial implica la corrección total; esta distinción es esencial solo en programas que incluyan ciclos o recursiones.

Relación de fortalecimiento entre aserciones

Si R y S son dos aserciones, R es más fuerte que S (R ⇒ S) si todos los estados que satisfacen a R también satisfacen a S; ⇒ es la relación de fortalecimiento. Ejemplo: { i > 1 } ⇒ { i > 0 }, ya que siempre que i > 1 se cumple i > 0.

Fortalecer una aserción disminuye el número de estados que la satisfacen: más fuerte = más selectivo, específico y restrictivo; más débil = menos selectivo, más general y menos restrictivo. La aserción más débil es la vacía { } (constante lógica V = true); la más fuerte es F (false).

Algunas reglas: si R ⇒ S y K es una aseveración cualquiera, entonces { R, K } ⇒ { S, K } (ej.: { i > 5 } ⇒ { i > 0 }, y con K = { j > 3 }: { i > 5, j > 3 } ⇒ { i > 0, j > 3 }); la relación es transitiva (si R ⇒ S y S ⇒ T, entonces R ⇒ T); A ⇒ A; p ⇒ (p ∨ q). De A ⇒ B no se sigue B ⇒ A: { y = 4 } ⇒ { y ≠ 0 }, pero { y ≠ 0 } no implica { y = 4 }; y { a = b } implica la disyunción { a > b } ∨ { a < b }, pero la disyunción no implica { a = b }.

Reglas de inferencia de las ternas de Hoare

• Fortalecimiento de precondiciones: si {P} C {Q} es correcto y P1 ⇒ P, entonces {P1} C {Q} es correcto. Ejemplo: como { y ≠ 0 } x := 1/y { x = 1/y } es correcta y { y = 4 } ⇒ { y ≠ 0 }, entonces { y = 4 } x := 1/y { x = 1/y } también lo es. Fortalecer la precondición pasa a un conjunto más pequeño de valores; debilitarla, a uno más grande. La aserción vacía puede reforzarse para producir cualquier precondición: de { } a := b { a = b } se deduce { P } a := b { a = b } para cualquier { P }.
• Debilitamiento de postcondiciones: si {P} C {Q} es correcto y Q ⇒ Q1, entonces {P} C {Q1} es correcto. Ejemplo: de { } max := b { max = b } y { max = b } ⇒ { max ≥ b } se deduce { } max := b { max ≥ b }.
• Conjunción de precondiciones: si {P1} C {Q1} y {P2} C {Q2} son correctas, entonces {P1 ∧ P2} C {Q1 ∧ Q2} es correcta. Caso particular: de { } C { Q1 } y { P2 } C { Q2 } se deduce { P2 } C { Q1 ∧ Q2 }. Ejemplo: de { } i := i + 1 { i = i + 1 } y { i > 0 } i := i + 1 { i > 0 } se obtiene { i > 0 } i := i + 1 { i > 0 ∧ i = i + 1 }, y como esto implica { i > 1 }, por debilitamiento de postcondiciones se concluye { i > 0 } i := i + 1 { i > 1 }.
• Disyunción de precondiciones: si {P1} C {Q1} y {P2} C {Q2} son correctas, entonces {P1 ∨ P2} C {Q1 ∨ Q2} es correcta. Caso particular: de { } C { Q1 } y { P2 } C { Q2 } se deduce { P2 } C { Q1 ∨ Q2 }.

Cómo demostrar que un programa es correcto

Para demostrar que un programa es correcto se parte de la postcondición final del código (las condiciones que deben cumplir los resultados correctos) y a partir de ahí se deduce la precondición. El código se verifica en sentido contrario a como se ejecuta (hacia atrás). Si la precondición encontrada es igual a la precondición inicial del programa, el programa es correcto; en otro caso, es incorrecto.

Instrucciones de asignación: regla de inferencia

Las instrucciones de asignación son de la forma V := E, con V una variable y E una expresión, y cumplen: { } V := E { V = E }. Para hallar la precondición {P} de {P} V := E {Q} se sustituyen todas las ocurrencias de V en Q por E.

Ejemplos:

• Determinar P para que { P } i := 2·i { i < 6 } sea correcta: sustituyendo i por 2·i en la postcondición queda { 2·i < 6 } = { i < 3 }. Luego { i < 3 } i := 2·i { i < 6 } es correcta.
• Con k = 4·a, para { a = ? } k := 4·a { k = 12 }, la precondición es { 4·a = 12 } = { a = 3 }; es decir, { a = 3 } k := 4·a { k = 12 }.

De forma similar, dada la precondición {P}, la postcondición {Q} se halla sustituyendo en E los valores que las variables tienen en {P}: con { a = 3 } k := 4·a { k = ? }, sustituyendo a = 3 en k = 4·a queda k = 4 × 3 = 12, es decir, { k = 12 }.

2 Puntos destacados / Lo que hay que saber

3 Actividades y tareas pendientes

No se dejó en esta clase una tarea con fecha de entrega (la tarea de los cuadros mágicos corresponde al material de la clase anterior).

4 Dudas que podrían examinar

5 Sitios o recursos para visitar

• Lógica de Hoare — fundamentos matemáticos de la verificación formal de programas (ternas {P} C {Q}) (dominio: google.com).
• C. A. R. Hoare (QuickSort, Premio Turing 1980) — creador de las ternas de Hoare (dominio: google.com).
• Verificación formal de programas — corrección parcial, total y aserciones (dominio: google.com).
• Regla de la asignación (axioma de Hoare) — cómo hallar la precondición de una asignación V := E (dominio: google.com).

6 Glosario de términos

• Demostración formal de programas: aplicación de técnicas, métodos y resultados formales para demostrar que un programa es correcto
• Programa correcto: programa que, con los datos de entrada, produce la salida esperada; en esta definición no cuenta tiempo, recursos ni eficiencia
• Terna de Hoare: {P} C {Q}: precondición, código (instrucción o programa) y postcondición
• Precondición ({P}): aserción que establece las condiciones (valores iniciales) que deben cumplir los datos de entrada
• Postcondición ({Q}): aserción que establece las condiciones de salida aceptadas como solución correcta
• Aserción / aseveración: relación entre variables y constantes que describe el estado del programa en un punto
• Aserción vacía { }: aserción "verdadera para todos los estados"; es la más débil (constante lógica V = true)
• Estado: conjunto de valores que toman las variables en un instante; un programa transforma el estado inicial en uno final
• Satisfacción: un estado E satisface una aseveración P cuando los valores de las variables en E cumplen P
• Corrección parcial: {P} C {Q} es parcialmente correcto si, cuando C termina (empezando con un estado que satisface P), el estado final satisface Q
• Corrección total: corrección parcial más la garantía de que C siempre termina
• Relación de fortalecimiento (⇒): R es más fuerte que S (R ⇒ S) si todo estado que satisface R satisface S
• Fortalecer / debilitar: reforzar una aserción reduce los estados que la satisfacen (más selectiva); debilitarla los aumenta (más general)
• Regla de inferencia: regla lógica asociada a cada tipo de instrucción para deducir precondiciones/poscondiciones en las ternas de Hoare
• Fortalecimiento de precondiciones: si {P} C {Q} es correcta y P1 ⇒ P, entonces {P1} C {Q} es correcta
• Debilitamiento de postcondiciones: si {P} C {Q} es correcta y Q ⇒ Q1, entonces {P} C {Q1} es correcta
• Conjunción de precondiciones: de {P1} C {Q1} y {P2} C {Q2} se deduce {P1 ∧ P2} C {Q1 ∧ Q2}
• Disyunción de precondiciones: de {P1} C {Q1} y {P2} C {Q2} se deduce {P1 ∨ P2} C {Q1 ∨ Q2}
• Asignación (V := E): instrucción que cumple { } V := E { V = E }; su precondición se halla sustituyendo V por E en la postcondición

7 Mapa mental textual

• Programación Avanzada · Clase 4 — Demostración formal de programas (ternas de Hoare)
  • Demostración formal de programas
    • Programa correcto = produce la salida esperada (sin contar tiempo/recursos/eficiencia)
  • Ternas de Hoare ({P} C {Q})
    • Precondición {P} y postcondición {Q} (aserciones) · estados inicial/final · C1 ; C2
    • Aserción vacía { } (true) · propiedades
    • Ejemplos: { y ≠ 0 } x := 1/y { x = 1/y } · { } a := b { a = b }
    • C. A. R. Hoare (1934, QuickSort 1960, Premio Turing 1980)
  • Corrección
    • Parcial (cumple Q si termina) · Total (además siempre termina)
    • Sin ciclos → la parcial implica la total
  • Relación de fortalecimiento (R ⇒ S)
    • Más fuerte = más restrictivo · más débil = más general · vacía = lo más débil · F = lo más fuerte
    • Reglas: {R,K} ⇒ {S,K} · transitividad · A ⇒ A · p ⇒ p∨q
  • Reglas de inferencia de Hoare
    • Fortalecimiento de precondiciones (P1 ⇒ P)
    • Debilitamiento de postcondiciones (Q ⇒ Q1)
    • Conjunción (∧) y disyunción (∨) de precondiciones
  • Verificación de programas
    • Partir de la postcondición final · verificar hacia atrás
    • Coincide la precondición deducida con la inicial → correcto
  • Regla de la asignación V := E
    • { } V := E { V = E }
    • Hallar P sustituyendo V por E en Q: { i < 3 } i := 2·i { i < 6 }
    • Hallar Q sustituyendo valores de P: { a = 3 } k := 4·a { k = 12 }